specification sorts state; variables s : state; s0 : state; s1 : state; s2 : state; S : state flexible; end specification